We present a weakest-precondition-style calculus for reasoning about theexpected values (pre-expectations) of \emph{mixed-sign unbounded} randomvariables after execution of a probabilistic program. The semantics of awhile-loop is well-defined as the limit of iteratively applying a functional toa zero-element just as in the traditional weakest pre-expectation calculus,even though a standard least fixed point argument is not applicable in thiscontext. A striking feature of our semantics is that it is always well-defined,even if the expected values do not exist. We show that the calculus is sound,allows for compositional reasoning, and present an invariant-based approach forreasoning about pre-expectations of loops.
展开▼
